Implement model for String.equals #7
Conversation
codebyzeb
requested review from
peterschrammel,
Degiorgio,
dcattaruzza and
allredj
src/main/java/java/lang/String.java
Outdated
| @@ -1393,8 +1393,10 @@ else if(c<=0xFFFF) | |||
| * @diffblue.untested | |||
There was a problem hiding this comment.
Why is this tagged untested?
codebyzeb
force-pushed
the
zgoriely/string-equals
branch
2 times, most recently
from
ce59649 to
66202de
Compare
romainbrenguier
force-pushed
the
zgoriely/string-equals
branch
from
66202de to
c77e6a1
Compare
| @@ -1611,7 +1612,7 @@ public int compareTo(String anotherString) { | |||
| // DIFFBLUE MODEL LIBRARY For some reason this needs to be not null for | |||
| // FileReader tests to pass. | |||
| public static final Comparator<String> CASE_INSENSITIVE_ORDER | |||
| = CProver.nondetWithoutNullForNotModelled(); | |||
| = null; | |||
There was a problem hiding this comment.
the comment directly above needs to be updated
There was a problem hiding this comment.
I don't see why this change is necessary or related to this PR?
There was a problem hiding this comment.
Some JBMC tests fail because the type on the left and right correspond (for jbmc). This wasn't a problem before but if we load the model of String.java for using String.equals this also gets loaded.
| @@ -1611,7 +1612,7 @@ public int compareTo(String anotherString) { | |||
| // DIFFBLUE MODEL LIBRARY For some reason this needs to be not null for | |||
| // FileReader tests to pass. | |||
| public static final Comparator<String> CASE_INSENSITIVE_ORDER | |||
| = CProver.nondetWithoutNullForNotModelled(); | |||
| = null; | |||
There was a problem hiding this comment.
I don't see why this change is necessary or related to this PR?
| */ | ||
| public boolean equals(Object anObject) { | ||
| // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC | ||
| return CProver.nondetBoolean(); | ||
| if (anObject instanceof String) { |
There was a problem hiding this comment.
As in the models-lib PR, could you add the original code from the JDK, commented out?
romainbrenguier
force-pushed
the
zgoriely/string-equals
branch
from
7665490 to
d6b8a38
Compare
| // } | ||
| // return false; | ||
|
|
||
| // DIFFBLUE MODEL LIBRARY Use CProverString function |
There was a problem hiding this comment.
⛏️ In the other PR, it says "method" instead of "function".
There was a problem hiding this comment.
corrected in the other PR
String.equals is currently handled internally by CBMC, here we update the model so that String.equals is supported when we move support to models-library.
romainbrenguier
force-pushed
the
zgoriely/string-equals
branch
from
d6b8a38 to
97aaf65
Compare
String.equals is currently handled internally by CBMC, here we update
the model so that String.equals is supported when we move support
to models-library.